(declare-fun a () Real)
(declare-fun b () Real)
(assert (> a 0))
(assert (>= b 6))
(push)
(assert (< (* (* 5 b) a (* 5 a)) 5))
(check-sat)
(assert (> a 0))
(assert (>= b 6))
(push)
(assert (< (* (* 5 b) a (* 5 a)) 5))
(check-sat)
